es-p-immediate-pred(es;P)(e,e')
== (e' < e) & P(e) & P(e') & (e'':E. (e'' < e)  (e' < e'')  ((P(e'')))) 

latex

---

clarification:

es-p-immediate-pred(es;P)(e,e')
== es-causl(es; e'; e)
== & P(e)
== & P(e')
== & (e'':es-E(es). es-causl(es; e''; e)  es-causl(es; e'; e'')  ((P(e'')))) 

latex

Definitions	x.A(x), P & Q, x:A. B(x), E, P  Q, (e < e'), A, f(a)
FDL editor aliases	es-p-immediate-pred